$\forall$$n$, $k$:$\mathbb{N}$, $c$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$).
\\[0ex]$\exists$$p$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow$($\mathbb{N}$ List)).
\\[0ex]sum($\parallel$$p$($j$)$\parallel$ $\mid$ $j$ $<$ $k$) $=$ $n$ $\in$ $\mathbb{Z}$
\\[0ex]\& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$, $x$, $y$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$p$($j$)$\parallel$}}$. $x$$<$$y$ $\Rightarrow$ ($p$($j$))[$x$]$>$($p$($j$))[$y$])
\\[0ex]\& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$, $x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$p$($j$)$\parallel$}}$. ($p$($j$))[$x$]$<$$n$ \& $c$(($p$($j$))[$x$]) $=$ $j$ $\in$ $\mathbb{Z}$)